DESIGN BY CONTRACT™ (hereinafter, referred to as “DbC”) is a beneficial software development practice that, until now, was cumbersome to actually incorporate into most development processes. DbC is a formal way of using comments to incorporate specification information into the code itself. DbC was designed to create a contract between a piece of code and its caller. This contract specifies what the callee expects and what the caller can expect. Basically, the code specification is expressed unambiguously using a formal language that describes the code's implicit contracts. These contracts specify such requirements as:                Conditions that the client must meet before a method is invoked.        Conditions that a method must meet after it executes.        Invariants that program objects must satisfy at all times.        Assertions that a method must satisfy at specific points of its execution.        
DbC originated for Eiffel classes. Eiffel classes are components that cooperate through the use of the contract, which defines the obligations and benefits for each class. For an introduction to DbC, see “Object-Oriented Software Construction” by Bertrand Meyer Prentice Hall, ISBN 0-13-629155-4, the contents of which are hereby incorporated by reference. The contracts clearly document what each method requires and what it is required to do. This makes it possible to verify whether methods are used as expected and whether they deliver the results expected by other parts of the system.
Any piece of code in any language has implicit contracts attached to it. The simplest example of an implicit contract is a method for which a null is not supposed to be passed. If this contract is not met, a NullPointerException occurs. Another example is a component whose specification states that it only returns positive values. If it occasionally returns negative values and the consumer of this component is expecting the functionality described in the specification (only positive values returned), this contract violation could lead to a critical problem in the application. Applying DbC to a code has significant benefits including:                The code's assumptions are clearly documented (for example, an item should not be null). Design concepts are placed directly in the code itself.        The code's contracts can be checked for consistency because they are explicit.        The code is much easier to reuse.        The specification will not be lost.        When programmers see the specification while writing the code, they are more likely to implement the specification correctly.        When programmers see the specification while modifying code, they are much less likely to introduce errors.        
However, conventional testing approaches have many disadvantages such as, black-box test cases must be created and updated each time the code's specification changes, and class/component misuse is difficult to be detected. Moreover, the class implementation can be cumbersome and there is no guarantee that the results will satisfy the post-conditions of the class client. Therefore, there is a need for a software tool to automatically check the implementation of contracts and to verify that a code functions in an expected way, particularly, in a target system.